2018-06-08

Построение категорий от Set до ∞

После первой 2-часовой лекции по MLTT, где детально разбираются Пи, Сигма, Путь и все их компоненты [Formation, Inro, Elim, Rec, Case, Induction, Eta, Beta] (а у Пути еще дополнительных куча subst, trans, все конечно через J выражаются, но через J реально никто не пишет, поэтому надо учить сразу культурке). У Пи типа есть еще funExt аксиома без которой не доказывается, что тип морфизмов является множеством, поэтому конструктивное построение инфинити категорий было невозможно до agda --cubical. Если морфизмы образуют не множество, а групоид, то это уже будет другая категория и так дальше до инфинити групоида. Кроме этого категории еще вкладываются друг в друга, например 0-категория — это множества или сетоид, где отношение Hom A B — это отношение эквивалентности на множествах, 1-категория, это категория где объекты — это 0-категории, множества или топологические пространства, а морфизмы — это отображения, в 2-категориях объекты — это 1-категории или просто категории, 1-морфизмы — это функторы, а 2-морфизмы — это естественные преобразования. На втором уроке можно уже строить категорию Множеств. Ну а категорию функторов можно давать уже после полного введения в теорию категори с лимитами. И уже только после теорката и категории функторов можно прееходить к семантике зависимой теории, категории контекстов, где морфизмы — это подстановки и категориям с семействами. Только сейчас решил написать это.

The general notion of (∞,1)-categories


 -- 0-cat   -- 0-ob are elements, 0-hom is equivalence relation, setoid -- sets
 -- 1-cat   -- 1-ob are spaces or 0-cat, 1-hom are maps
 -- 2-cat-A -- 2-ob are 1-cat, 1-hom are functors/maps        \ bounded
 -- 2-cat-B -- 2-ob are 1-cat, 2-hom are ntrans/mapsOnMaps    / definition
 -- 3-cat-A -- 2-ob are (2-cat-A,2-cat-B), 1-hom are functors of prod categories \
 -- 3-cat-B -- 2-ob are (2-cat-A,2-cat-B), 2-hom are ntrans of prodcategories     |
 -- 3-cat-C -- 3-ob are (2-cat-A,2-cat-B), 3-hom are modifications               /

Enrichment


 --   (0-cat = Hom(A,B)         = A = B)
 -- ↪ (1-cat = Hom(0-cat,0-cat) = set -> 0-cat)
 -- ↪ (2-cat = Hom(1-cat,1-cat) = (set -> 0-cat) -> 1-cat)
 -- ↪ (3-cat = Hom(2-cat,2-cat) = ((set -> 0-cat) -> 1-cat) -> 2-cat)

The general notion of k-morphisms


 -- equiv        0-hom: U
 -- functor      1-hom (C D: 1-cat): U
 -- ntrans       2-hom (C D: 1-cat) (F G: 1-hom C D): U
 -- modification 3-hom (C D: 1-cat) (F G: 1-hom C D) (I J: 2-hom C D F G): U

1-Category of Sets


Set: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = SET
    Hom (A B: Ob): U = A.1 -> B.1
    id (A: Ob): Hom A A = idfun A.1
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = o A.1 B.1 C.1 g f
    HomSet (A B: Ob): isSet (Hom A B) = setFun A.1 B.1 B.2
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) f
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
     : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
     = refl (Hom A D) (c A B D f (c B C D g h))


 Functions (X Y: U) (Z: isSet Y): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q)
   where
     Ob: U = X -> Y
     Hom (A B: Ob): U = id (X -> Y)
     id (A: Ob): Hom A A = idfun (X -> Y)
     c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = idfun (X -> Y)
     HomSet (A B: Ob): isSet (Hom A B) = setFun Ob Ob (setFun X Y Z)
     L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined
     R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined
     Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))

2-Category with 1-hom morphisms (functors)


 Cat: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = precategory
    Hom (A B: Ob): U = catfunctor A B
    id (A: Ob): catfunctor A A = idFunctor A
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = compFunctor A B C f g
    HomSet (A B: Ob): isSet (Hom A B) = undefined
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))

AwodeyCT Definition 7.9. The functor category 2-Category of Functors F: X -> Y with 2-hom morphisms (natural transformations).


 Func (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = catfunctor X Y
    Hom (A B: Ob): U = ntrans X Y A B
    id (A: Ob): ntrans X Y A A = undefined
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C = undefined
    HomSet (A B: Ob): isSet (Hom A B) = undefined
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = undefined
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = undefined
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))

Category of Abelian Groups


 Ab: precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    Ob: U = abgroup
    Hom (A B: Ob): U = abgrouphom A B
    id (A: Ob): Hom A A = idmonoidhom (A.1, A.2.1.1)
    c (A B C: Ob) (f: Hom A B) (g: Hom B C): Hom A C
      = monoidhomcomp (A.1, A.2.1.1) (B.1, B.2.1.1) (C.1, C.2.1.1) f g
    HomSet (A B: Ob): isSet (Hom A B) = setmonoidhom (A.1,A.2.1.1) (B.1,B.2.1.1)
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f
      = lemma_idmonoidhom0 (A.1, A.2.1.1) (B.1, B.2.1.1) f
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f
      = lemma_idmonoidhom1 (A.1, A.2.1.1) (B.1, B.2.1.1) f
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
       = lemma_monoidcomp0(A.1,A.2.1.1)(B.1,B.2.1.1)(C.1,C.2.1.1)(D.1,D.2.1.1)f g h

Product Category of two Categories


 Product (X Y: precategory): precategory = ((Ob,Hom),id,c,HomSet,L,R,Q) where
    x: U = carrier X
    y: U = carrier Y
    Ob: U = prod x y
    Hom (A B: Ob): U = prod (id x) (id y)
    id (A: Ob): Hom A A = (idfun x, idfun y)
    c (A B C: Ob) (f: Hom A B) (g: Hom B C):
      Hom A C = (o x x x f.1 g.1, o y y y f.2 g.2)
    HomSet (A B: Ob): isSet (Hom A B) = undefined
    L (A B: Ob) (f: Hom A B): Path (Hom A B) (c A A B (id A) f) f = refl (Hom A B) f
    R (A B: Ob) (f: Hom A B): Path (Hom A B) (c A B B f (id B)) f = refl (Hom A B) f
    Q (A B C D: Ob) (f: Hom A B) (g: Hom B C) (h: Hom C D)
       : Path (Hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
       = refl (Hom A D) (c A C D (c A B C f g) h)

Почему категорию множеств можно давать сразу на втором уроке без теорката? Потому, что в доказательствах свойств категории испольется только refl, такой же фокус как и с инференс правилами встроенной теории типов (самодоказательство, пруф чекинг тайп чекера по сути). Остается только детально разбрать доказательствао setFun которое говорит, что если кодомен множество, то стрелка тоже множество, ну а у нас не только кодомен множество, но и домен, так что доказательство тоже тривиальное, и как раз оно требует funExt.

Сама структура SET тоже непростая, и для общей реализации надо использовать n-groupoid, так как isSet предикат в SET = (X: U) * isSet X — это 0-групоид. Благо это все можно рассказать на первом уроке. Объектами 3-категория будет 2-тапл 2-категорий и дальше по индукции. Просто начиная с 4-категории уже начинает резко нехватать бумаги из-за симплициальной струтктуры инфинити категорий, и непонятно, кому и зачем это может понадобиться. Думаю можно написать генератор сигнатур для инфинити категорий. Но только через метапрограммирование, напрямую AST генерировать, эффективнее всего. Вот например башня из трех сигнатур по которой все понятно:

1-hom (C D: cat): U — сигнатура функтора
2-hom (C D: cat) (F G: 1-hom C D): U — сигнатура естественного преобразования
3-hom (C D: cat) (F G: 1-hom C D) (I J: 2-hom C D F G): U — сигнатура 3-морфизма

Для любителей матфизики, введение в n-категории Джона Баеза.

[1]. http://math.ucr.edu/home/baez/ncat.ps
[2]. http://web.stanford.edu/~arpon/math/files/inftycats-motivation.pdf
[3]. M.Sokhatskyi. Issue VII: Formal Topos on Category of Sets